perm filename CONTIN[W77,JMC] blob sn#270918 filedate 1977-03-18 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 00003	.skip 1
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.turn off "{"
.cb CONTINUOUS FUNCTIONALS AND THEIR LEAST FIXED POINTS


	According to the Scott-Strachey theory of recursive programs,
a recursive function like %2n!_=_factorial(n)%1
given by a conditional expression recursion like

!!a1:	%2factorial(n) ← qif n = 0 qthen 1 qelse n%8.%2factorial(n - 1)%1

is regarded as the least fixed point of a continuous functional

!!a2:	%2qt1 = λf.λn.(qif n = 0 qthen 1 qelse n%8.%2f(n - 1)%1.

We will assume the reader is familiar with the exposition of this
theory in (Manna 1974) or (Scott and deBakker 1970).

	Not all continuous functionals are of the simple kind
used in defining recursive programs, and the object of this paper
is to define this simple kind, give some examples of continuous
functionals that don't belong to it, study their least fixed points,
and give some conditions for a continuous functional to be of the
simple kind.

%3Definition 1%1 - %2A continuous functional is called simple if it
has the form

!!a3:	%2λf.λx.E%*

where ⊗E is a quantifier-free
term built up from base functions and predicates and a function symbol ⊗f 
by composition and conditional expressions%1.

	qt1 defined in ({eq a2}) is a simple functional.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of

PUBbed at {time} on {date}.%1